\begin{tabbing}
ma{-}feasible\=\{i:l\}\+
\\[0ex]($M$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fpf{-}all(Id; IdDeq; 1of($M$); $x$,$T$.$T$)\+
\\[0ex]\& fpf{-}all(Knd; KindDeq; 1of(2of($M$)); $k$,$T$.Dec($T$))
\\[0ex]\& fpf{-}all(\=Id;\+
\\[0ex]IdDeq;
\\[0ex]1of(2of(2of(2of($M$))));
\\[0ex]$a$,$p$.($\forall$$s$:State(1of($M$)).
\\[0ex]Dec($\exists$$v$:fpf{-}cap(1of(2of($M$));KindDeq;locl($a$);Top). $p$($s$,$v$))))
\-\\[0ex]\& fpf{-}all(Id; IdDeq; 1of($M$); $x$,$T$.AtomFree(Type$_{\mbox{\scriptsize i}}$;$T$))
\\[0ex]\& fpf{-}all(Knd; KindDeq; 1of(2of($M$)); $k$,$T$.AtomFree(Type$_{\mbox{\scriptsize i}}$;$T$))
\\[0ex]\& ma{-}frame{-}compat($M$;$M$)
\-
\end{tabbing}